felix.git/test/golden/inductive/encoding tasks.golden, branch hotg Unnamed repository; edit this file 'description' to name the repository. https://git.adelon.net/felix.git/atom?h=hotg 2026-08-03T19:00:28+00:00 Remove obsolete verification machinery 2026-08-03T19:00:28+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-08-03T19:00:28+00:00 urn:sha1:5cdde1fd0f976863ae4b5831ab389048138b06a4 Check direct inductives through fixed-point replay 2026-07-28T12:54:42+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-28T12:54:42+00:00 urn:sha1:ba4acdaa305d01469f66cd316edde4d22ea2fff9 Allocate task-local TPTP names 2026-07-27T17:50:15+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-27T15:59:05+00:00 urn:sha1:1a6f4ba1adc8e5f44d0b4973b6bcdb9b4e08de0f Distinct target variable names exposed a replacement-condition scope lift that source-derived names had masked. Keep those variables under the replacement existential. Remove source annotations from TPTP tasks 2026-07-27T16:19:29+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-27T02:42:09+00:00 urn:sha1:904ca07b7a89e3a91420876ef08e7113aae906e4 Use semantic subset formula inside inductive defns 2026-07-23T17:56:52+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-23T17:56:52+00:00 urn:sha1:d1d3f178db000a6ffd928a75af8eb1ba2b7f8b9a Track ownership of top-level symbols 2026-07-03T00:13:21+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-07-03T00:13:21+00:00 urn:sha1:40bc466d6a996e731cba21f24a58be08b1f22689 Require every ownable top-level symbol to be introduced by a dedicated owner before it can appear in facts. Reject duplicate ownership and prevent symbols used by inductive definitions from being defined later. Use the ownership/dependency information to reject hidden recursive inductive definitions and to generate referenceable inductive principles. BREAKING CHANGE: Top-level facts no longer introduce symbols implicitly. Use shorter `_local_N` marker in TPTP output 2026-02-24T15:15:26+00:00 adelon 22380201+adelon@users.noreply.github.com 2026-02-24T15:15:26+00:00 urn:sha1:330fa14bf6f075342cbe8e515d67740fd1edcf00 Fix column location 2025-12-14T16:54:05+00:00 adelon 22380201+adelon@users.noreply.github.com 2025-12-14T16:54:05+00:00 urn:sha1:8e7d2c94d8449b8512fd6257534b4c593319b4ae Add more location info in tasks 2025-12-14T16:47:51+00:00 adelon 22380201+adelon@users.noreply.github.com 2025-12-14T16:47:51+00:00 urn:sha1:4c536bc12666fb664ca522f99ea8f200963050c7 Add location info to conjecture 2025-12-14T02:37:11+00:00 adelon 22380201+adelon@users.noreply.github.com 2025-12-14T02:37:11+00:00 urn:sha1:3fe36e6f3266a7cfac51b56ead96c1e129a97ea9 Still some `<nowhere>` value as placeholder left over.